| Definitions | vartype(i;x), Id, loc(e), s = t, (x after e), pred(e), x when e, discrete(i;x), first(e), kind(e),   x. t(x), x,y. t(x;y), loc(e), first(e), suptype(S; T), S  T,  x:A.B(x), Void, SWellFounded(R(x;y)), pred!(e;e'), SqStable(P),  T, True, E, t.1, let x,y = A in B(x;y), Top, constant_function(f;A;B),  , r  s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time),  ,  , type List, Msg(M), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, EState(T), EOrderAxioms(E; pred?; info), IdLnk, left + right, Unit, @i(x:T), P    Q, P & Q, P Q, x:A  B(x), isrcv(e), f(a), SQType(T), {T}, s ~ t,  , t  T, e loc e' , <a, b>,  b, if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y),  A, False, Atom$n, ES, EqDecider(T), x:A  B(x), Type, {x:A| B(x)} ,  x:A. B(x), P Q, x changed before e, Decision, (last change to x before e), inr x ,  b, A c B, inl x , tt, ff, (e <loc e'), Dec(P), P  Q, e(e1,e2].P(e), @e(x v), (e < e'),  ,  e<e'.P(e), x:A. B(x) |
| Lemmas | es-after wf, squash wf, member wf, es-locl-iff, es-locl wf, assert-changed, es-le-pred, es-causle-le, bool sq, loc-last-change, es-le-not-locl, es-le weakening, es-locl transitivity2, es-pred-locl, last-change wf, decidable es-locl, last-change-property, inconsistent-bool-eq, changed wf, bfalse wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, inconsistent-bool-eq2, inl wf, btrue wf, false wf, true wf, decidable assert, sq stable from decidable, es-loc-pred, es-le-loc, es-vartype wf, es-isrcv-loc, es-after-pred, sq stable subtype rel, es-pred wf, es-loc wf, Id sq, assert wf, iff wf, bool wf, event system wf, unit wf, top wf, first wf, not wf, constant function wf, EState wf, IdLnk wf, kindcase wf, Knd wf, rationals wf, qle wf, cless wf, val-axiom wf, nat wf, Msg wf, loc wf, kind wf, Id wf, EOrderAxioms wf, deq wf, es-dtype wf, es-E wf, es-first wf, es-isconst wf, es-when wf |
